Inference at * 1 1 1 
Iof proof for Lemma before-hd:



1. T : Type
2. L : T List
3. 0 < ||L||
4. no_repeats(T;L)
5. x : T
6. x before hd(L)  L
7. x, y:T. x before y  L  ((x = y))
8. (x = hd(L))
9. hd(L) before x  L
10. x before x  L
  False 

latex

 by InteriorProof ((FHyp (-4) [-1]) 
CollapseTHENA (Auto)) 

latex

C1: 

C1: 11. (x = x)
C1:   False
C.

Definitions

x:A. B(x), P  Q, x:AB(x), A